Why remove?

See 710f088; currently git submodules are put in .ciignore to maintain reproducibility between local users and CI. For example, if a user runs generate_manifest.py locally when contributing their specs but did not clone the repo with submodules (common), the generated manifest will skip including all the submodules.

See 710f088; currently git submodules are put in .ciignore to maintain reproducibility between local users and CI. For example, if a user runs generate_manifest.py locally when contributing their specs but did not clone the repo with submodules (common), the generated manifest will skip including all the submodules.

The vast majority of users accessing the Example repository aren't concerned with the manifest.json file; they're primarily interested in the examples as a means of learning TLA+. Therefore, concerns about manifest generation shouldn't justify removing existing automation that checks that the examples work.

The other submodules were removed from CI checking for similar reasons. If we want the submodules to be included in the CI then they should be moved inside the repository. Possibly this would be less of an issue if we go to a devolved per-directory manifest.json file as suggested in #171, but then the people would be required to add a manifest.json file to their actual repository that is being submoduled.

The other submodules were removed from CI checking for similar reasons. If we want the submodules to be included in the CI then they should be moved inside the repository. Possibly this would be less of an issue if we go to a devolved per-directory manifest.json file as suggested in #171, but then the people would be required to add a manifest.json file to their actual repository that is being submoduled.

There will always be spec that are referenced but not included directly in this repository for various reasons. Fortunately, Git submodules provide a relatively stable form of reference, as they capture not only the location of the external repo but also a specific commit in time. This minimizes the risk of CI brittleness—especially when the referenced spec is also hosted on GitHub.

In this case, the Microwave example was checked before this PR to ensure it works as expected for the primary audience of this repository. Therefore, please revert this PR.

Perhaps we can discuss handling submodule specs as part of a more comprehensive change in #171. Your suggestions in #169 (comment) of moving manifests to spec preamble/postamble would also not work with submodules as described, unless the origin repository is modified, in which case might as well bring the specs into this repo. It makes sense to unify these discussions instead of keeping them separate.

Also to be clear: this change did not remove the microwave example. It just removed it from CI validation. Since, as you said, submodules capture a snapshot of the spec, and it was validated once, it will remain valid for the primary audience of this repository (presumably, users wanting to look at specifications).